$\forall$$M$:MsgA. $M$.state $\in$ Type